<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Libraries initialisation & threading | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/Tutorials/">
              <span property="name"><b>Tutorials</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Libraries initialisation & threading</span>
            <meta property="position" content="3" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    

<div class="sidebar">
  <ul class="nav nav-sidebar tutorial-sidebar">
    <li class="nav-section">Getting started</li>
      <li><a href="/Tutorials/">Overview</a></li>
      <li><a href="/Tutorials/pathways">Tutorial pathways</a></li>
    <li class="nav-section">seL4</li>
      <li><a href="/Tutorials/setting-up">Setting up your machine</a></li>
      <li><a href="/Tutorials/get-the-tutorials">Getting the tutorials</a></li>
      <li><a href="/Tutorials/hello-world">Hello world</a></li>
      <li><a href="/Tutorials/capabilities">Capabilities</a></li>
      <li><a href="/Tutorials/untyped">Untyped</a></li>
      <li><a href="/Tutorials/mapping">Mapping</a></li>
      <li><a href="/Tutorials/threads">Threads</a></li>
      <li><a href="/Tutorials/ipc">IPC</a></li>
      <li><a href="/Tutorials/notifications">Notifications</a></li>
      <li><a href="/Tutorials/interrupts">Interrupts</a></li>
      <li><a href="/Tutorials/fault-handlers">Fault handling</a></li>
      <li><a href="/Tutorials/mcs">MCS extensions</a></li>
    <li class="nav-section">C Libraries</li>
      <li><a href="/Tutorials/libraries-1">Initialisation &amp; threading</a></li>
      <li><a href="/Tutorials/libraries-2">IPC</a></li>
      <li><a href="/Tutorials/libraries-3">Processes &amp; Elf loading</a></li>
      <li><a href="/Tutorials/libraries-4">Timer</a></li>
    <li class="nav-section">Microkit</li>
      <li><a href="https://trustworthy.systems/projects/microkit/tutorial/">Tutorial</a></li>
    <li class="nav-section">CAmkES</li>
      <li><a href="/Tutorials/hello-camkes-0">Hello CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-1">Introduction to CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-2">Events in CAmkES</a></li>
      <li><a href="/Tutorials/hello-camkes-timer">CAmkES timer tutorial</a></li>
      <li><a href="/Tutorials/camkes-vm-linux">CAmkES VM</a></li>
      <li><a href="/Tutorials/camkes-vm-crossvm">CAmkES cross-VM connectors</a></li>
    <li class="nav-section">Rust</li>
      <li><a href="https://github.com/seL4/rust-sel4">GitHub</a></li>
    <li class="nav-section">Resources</li>
      <li><a href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">seL4 Manual</a></li>
      <li><a href="/projects/sel4/api-doc.html">seL4 API reference</a></li>
      <li><a href="/Tutorials/how-to">How to: a quick solutions guide</a></li>
      <li><a href="/projects/sel4-tutorials/debugging-guide">Debugging guide</a></li>
      <li><a href="/Resources#contact">Help contacts</a></li>
  </ul>
</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">

    
<!--
  Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)

  SPDX-License-Identifier: BSD-2-Clause
-->

<h1 id="sel4-libraries-initialisation--threading">seL4 Libraries: Initialisation &amp; Threading</h1>

<p>This tutorial provides code examples and exercises for using the libraries
found in <a href="https://github.com/seL4/seL4_libs"><code class="language-plaintext highlighter-rouge">seL4_libs</code></a> to bootstrap a system and start a thread.</p>

<p>The tutorial is useful in that
it addresses conceptual problems for two different types of developers:</p>

<ul>
  <li>Experienced kernel developers whose minds are pre-programmed to
    think in terms of “One address space equals one process”, and
    begins to introduce the seL4 CSpace vs VSpace model.</li>
  <li>New kernel developers, for whom the tutorial will provide prompts on what to read.</li>
</ul>

<p>Don’t gloss over the globals declared before <code class="language-plaintext highlighter-rouge">main()</code> – they’re declared
for your benefit so you can grasp some of the basic data structures.</p>

<p>Outcomes:</p>
<ul>
  <li>Understand the kernel’s startup procedure.</li>
  <li>Understand that the kernel centers around certain objects and
      capabilities to those objects.</li>
  <li>Understand that libraries exist to automate the very
      fine-grained nature of the seL4 API, and get a rough idea of
      some of those libraries.</li>
  <li>Learn how the kernel hands over control to userspace.</li>
  <li>Get a feel for how the seL4 API enables developers to manipulate
      the objects referred to by the capabilities they encounter.</li>
  <li>Understand the how to spawn new threads in seL4, and the basic
      idea that a thread has a TCB, VSpace and CSpace, and that you
      must fill these out.</li>
</ul>

<h2 id="prerequisites">Prerequisites</h2>

<ol>
  <li><a href="/Tutorials/setting-up">Set up your machine</a></li>
  <li><a href="/Tutorials/hello-world">Hello world tutorial</a></li>
</ol>

<h2 id="initialising">Initialising</h2>

<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--tut</span> libraries-1
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-1_build
ninja
</code></pre></div></div>

<details>
  <summary><em>Hint:</em> tutorial solutions</summary>
  <p><br />
All tutorials come with complete solutions. To get solutions run:</p>

  <div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="c"># For instructions about obtaining the tutorial sources see https://docs.sel4.systems/Tutorials/get-the-tutorials</span>
<span class="c">#</span>
<span class="c"># Follow these instructions to initialise the tutorial</span>
<span class="c"># initialising the build directory with a tutorial exercise</span>
./init <span class="nt">--solution</span> <span class="nt">--tut</span> libraries-1
<span class="c"># building the tutorial exercise</span>
<span class="nb">cd </span>libraries-1_build
ninja
</code></pre></div>  </div>

  <p>Answers are also available in drop down menus under each section.</p>
</details>

<h2 id="exercises">Exercises</h2>

<p>When you first run the tutorial, you should see the following output:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Booting all finished, dropped to user space
main@main.c:89 [Cond failed: info == NULL]
Failed to get bootinfo.
</code></pre></div></div>

<h3 id="obtain-bootinfo">Obtain BootInfo</h3>

<p>After bootstrapping the system, the seL4 kernel hands over control to the root task.
 to an init thread.
This thread receives a structure from the kernel that describes all the
resources available on the machine. This structure is called the
BootInfo structure. It includes information on all IRQs, memory, and
IO-Ports (x86). This structure also tells the init thread where certain
important capability references are. This step is teaching you how to
obtain that structure.</p>

<p><code class="language-plaintext highlighter-rouge">seL4_BootInfo* platsupport_get_bootinfo(void)</code> is a function that returns the BootInfo structure.
It also sets up the IPC buffer so that it can perform some syscalls such as <code class="language-plaintext highlighter-rouge">seL4_DebugNameThread</code> used by <code class="language-plaintext highlighter-rouge">name_thread</code>.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo_types.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo_types.h</a></li>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/bootinfo.c">https://github.com/seL4/seL4_libs/blob/master/libsel4platsupport/src/bootinfo.c</a></li>
</ul>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 1: get boot info */</span>
    <span class="cm">/* hint: platsupport_get_bootinfo()
     * seL4_BootInfo* platsupport_get_bootinfo(void);
     * @return Pointer to the bootinfo, NULL on failure
     */</span>
<span class="err">}</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">info</span> <span class="o">=</span> <span class="n">platsupport_get_bootinfo</span><span class="p">();</span>
</code></pre></div>  </div>
</details>

<p>On success, you should see the following:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>libraries-1: main@main.c:124 [Cond failed: allocman == NULL]
	Failed to initialize alloc manager.
	Memory pool sufficiently sized?
	Memory pool pointer valid?
</code></pre></div></div>

<h3 id="initialise-simple">Initialise simple</h3>

<p><code class="language-plaintext highlighter-rouge">libsel4simple</code> provides an abstraction for the boot environment of a thread.
You need to initialize it with some default state before using it.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4simple-default/include/simple-default/simple-default.h">https://github.com/seL4/seL4_libs/blob/master/libsel4simple-default/include/simple-default/simple-default.h</a>
    <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
 <span class="cm">/* TASK 2: initialise simple object */</span>
 <span class="cm">/* hint: simple_default_init_bootinfo()
  * void simple_default_init_bootinfo(simple_t *simple, seL4_BootInfo *bi);
  * @param simple Structure for the simple interface object. This gets initialised.
  * @param bi Pointer to the bootinfo describing what resources are available
  */</span>
</code></pre></div>    </div>
  </li>
</ul>
<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">simple_default_init_bootinfo</span><span class="p">(</span><span class="o">&amp;</span><span class="n">simple</span><span class="p">,</span> <span class="n">info</span><span class="p">);</span>
</code></pre></div>  </div>
</details>
<p>On successful completion of this task, the output should not change.</p>

<h3 id="use-simple-to-print-bootinfo">Use simple to print BootInfo</h3>

<p>Use a <code class="language-plaintext highlighter-rouge">simple</code> function to print out the contents of the <code class="language-plaintext highlighter-rouge">seL4_BootInfo</code> function.</p>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 3: print out bootinfo and other info about simple */</span>
    <span class="cm">/* hint: simple_print()
     * void simple_print(simple_t *simple);
     * @param simple Pointer to simple interface.
     */</span>

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">simple_print</span><span class="p">(</span><span class="o">&amp;</span><span class="n">simple</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h">https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h</a></li>
</ul>

<p>The error message should remain, but your output should now also contain something like:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Node 0 of 1
IOPT levels:     4294967295
IPC buffer:      0x52c000
Empty slots:     [406 --&gt; 4096)
sharedFrames:    [0 --&gt; 0)
userImageFrames: [16 --&gt; 316)
userImagePaging: [12 --&gt; 15)
untypeds:        [316 --&gt; 406)
Initial thread domain: 0
Initial thread cnode size:
libraries-1: main@main.c:126 [Cond failed: allocman == NULL]
</code></pre></div></div>

<h3 id="initialise-an-allocator">Initialise an allocator</h3>

<p>In seL4, memory management is delegated in large part to userspace, and
each thread manages its own page faults with a custom pager. Without
the use of the <code class="language-plaintext highlighter-rouge">allocman</code> library and the <code class="language-plaintext highlighter-rouge">VKA</code> library, you would have to
manually allocate a frame, then map the frame into a page-table, before
you could use new memory in your address space. In this tutorial you
don’t go through that procedure, but you’ll encounter it later. For now,
use the allocman and VKA allocation system. The allocman library
requires some initial memory to bootstrap its metadata. Complete this
step.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/bootstrap.h">https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/bootstrap.h</a></li>
</ul>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 4: create an allocator */</span>
    <span class="cm">/* hint: bootstrap_use_current_simple()
     * allocman_t *bootstrap_use_current_simple(simple_t *simple, uint32_t pool_size, char *pool);
     * @param simple Pointer to simple interface.
     * @param pool_size Size of the initial memory pool.
     * @param pool Initial memory pool.
     * @return returns NULL on error
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">allocman</span> <span class="o">=</span> <span class="n">bootstrap_use_current_simple</span><span class="p">(</span><span class="o">&amp;</span><span class="n">simple</span><span class="p">,</span> <span class="n">ALLOCATOR_STATIC_POOL_SIZE</span><span class="p">,</span> <span class="n">allocator_mem_pool</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>The output should now be as follows:</p>

<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>&lt;&lt;seL4(CPU 0) [decodeInvocation/530 T0xffffff801ffb5400 "libraries-1" @401303]: Attempted to invoke a null cap #0.&gt;&gt;
libraries-1: main@main.c:199 [Err seL4_InvalidCapability]:
	Failed to set the priority for the new TCB object.
</code></pre></div></div>

<h3 id="obtain-a-generic-allocation-interface-vka">Obtain a generic allocation interface (vka)</h3>

<p><code class="language-plaintext highlighter-rouge">libsel4vka</code> is an seL4 type-aware object allocator that will allocate new
kernel objects for you. The term “allocate new kernel objects” in seL4
is a more detailed process of “retyping” previously un-typed memory.
seL4 considers all memory that hasn’t been explicitly earmarked for a
purpose to be “untyped”, and in order to repurpose any memory into a
useful object, you must give it an seL4-specific type. This is retyping,
and the VKA library simplifies this for you, among other things.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/vka.h">https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/vka.h</a></li>
</ul>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 5: create a vka (interface for interacting with the underlying allocator) */</span>
    <span class="cm">/* hint: allocman_make_vka()
     * void allocman_make_vka(vka_t *vka, allocman_t *alloc);
     * @param vka Structure for the vka interface object.  This gets initialised.
     * @param alloc allocator to be used with this vka
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">allocman_make_vka</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="n">allocman</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>On successful completion this task, the output should not change.</p>

<h3 id="find-the-cspace-root-cap">Find the CSpace root cap</h3>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 6: get our cspace root cnode */</span>
    <span class="cm">/* hint: simple_get_cnode()
     * seL4_CPtr simple_get_cnode(simple_t *simple);
     * @param simple Pointer to simple interface.
     * @return The cnode backing the simple interface. no failure.
     */</span>
    <span class="n">seL4_CPtr</span> <span class="n">cspace_cap</span><span class="p">;</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">cspace_cap</span> <span class="o">=</span> <span class="n">simple_get_cnode</span><span class="p">(</span><span class="o">&amp;</span><span class="n">simple</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>This is where the differences between seL4 and contemporary kernels
begin to start playing out. Every kernel-object that you “retype” will
be handed to you using a capability reference. The seL4 kernel keeps
multiple trees of these capabilities. Each separate tree of capabilities
is called a “CSpace”. Each thread can have its own CSpace, or a CSpace
can be shared among multiple threads. The delineations between
“Processes” aren’t well-defined, since seL4 doesn’t have any real
concept of “processes”. It deals with threads. Sharing and isolation is
based on CSpaces (shared vs not-shared) and VSpaces (shared vs
not-shared). The “process” idea goes as far as perhaps the fact that at
the hardware level, threads sharing the same VSpace are in a traditional
sense, siblings, but logically in seL4, there is no concept of
“Processes” really.</p>

<p>So you’re being made to grab a reference to your thread’s CSpace’s root
“CNode”. A CNode is one of the many blocks of capabilities that make up
a CSpace.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h">https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>

<h3 id="find-the-vspace-root-cap">Find the VSpace root cap</h3>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 7: get our vspace root page diretory */</span>
    <span class="cm">/* hint: simple_get_pd()
     * seL4_CPtr simple_get_pd(simple_t *simple);
     * @param simple Pointer to simple interface.
     * @return The vspace (PD) backing the simple interface. no failure.
     */</span>
    <span class="n">seL4_CPtr</span> <span class="n">pd_cap</span><span class="p">;</span>

</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">pd_cap</span> <span class="o">=</span> <span class="n">simple_get_pd</span><span class="p">(</span><span class="o">&amp;</span><span class="n">simple</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>Just as in the previous step, you were made to grab a reference to the
root of your thread’s CSpace, now you’re being made to grab a reference
to the root of your thread’s VSpace.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h">https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>

<h3 id="allocate-a-tcb-object">Allocate a TCB Object</h3>

<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 8: create a new TCB */</span>
    <span class="cm">/* hint: vka_alloc_tcb()
     * int vka_alloc_tcb(vka_t *vka, vka_object_t *result);
     * @param vka Pointer to vka interface.
     * @param result Structure for the TCB object.  This gets initialised.
     * @return 0 on success
     */</span>
    <span class="n">vka_object_t</span> <span class="n">tcb_object</span> <span class="o">=</span> <span class="p">{</span><span class="mi">0</span><span class="p">};</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">vka_alloc_tcb</span><span class="p">(</span><span class="o">&amp;</span><span class="n">vka</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">tcb_object</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>In order to manage the threads that are created in seL4, the seL4 kernel
keeps track of TCB (Thread Control Block) objects. Each of these
represents a schedulable executable resource. Unlike other contemporary
kernels, seL4 <strong>doesn’t</strong> allocate a stack, virtual-address space
(VSpace) and other metadata on your behalf. This step creates a TCB,
which is a very bare-bones, primitive resource, which requires you to
still manually fill it out.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h">https://github.com/seL4/seL4_libs/blob/master/libsel4vka/include/vka/object.h</a></li>
</ul>

<p>After completing this task, the errors should disappear, and you should see the following
output:</p>
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>main: hello world
</code></pre></div></div>

<h3 id="configure-the-new-tcb">Configure the new TCB</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
   <span class="cm">/* TASK 9: initialise the new TCB */</span>
    <span class="cm">/* hint 1: seL4_TCB_Configure()
     * int seL4_TCB_Configure(seL4_TCB _service, seL4_Word fault_ep, seL4_CNode cspace_root, seL4_Word cspace_root_data, seL4_CNode vspace_root, seL4_Word vspace_root_data, seL4_Word buffer, seL4_CPtr bufferFrame)
     * @param service Capability to the TCB which is being operated on.
     * @param fault_ep Endpoint which receives IPCs when this thread faults (must be in TCB's cspace).
     * @param cspace_root The new CSpace root.
     * @param cspace_root_data Optionally set the guard and guard size of the new root CNode. If set to zero, this parameter has no effect.
     * @param vspace_root The new VSpace root.
     * @param vspace_root_data Has no effect on IA-32 or ARM processors.
     * @param buffer Address of the thread's IPC buffer. Must be 512-byte aligned. The IPC buffer may not cross a page boundary.
     * @param bufferFrame Capability to a page containing the thread?s IPC buffer.
     * @return 0 on success.
     * Note: this function is generated during build.  It is generated from the following definition:
     *
     * hint 2: use seL4_CapNull for the fault endpoint
     * hint 3: use seL4_NilData for cspace and vspace data
     * hint 4: we don't need an IPC buffer frame or address yet
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_Configure</span><span class="p">(</span><span class="n">tcb_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="n">seL4_CapNull</span><span class="p">,</span>  <span class="n">cspace_cap</span><span class="p">,</span> <span class="n">seL4_NilData</span><span class="p">,</span> <span class="n">pd_cap</span><span class="p">,</span> <span class="n">seL4_NilData</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>You must create a new VSpace for your new thread if you need it to
execute in its own isolated address space, and tell the kernel which
VSpace you plan for the new thread to execute in. This opens up the
option for threads to share VSpaces. In similar fashion, you must also
tell the kernel which CSpace your new thread will use – whether it will
share a currently existing one, or whether you’ve created a new one for
it. That’s what you’re doing now.</p>

<p>In this particular example, you’re allowing the new thread to share your
main thread’s CSpace and VSpace.</p>

<p>In addition, a thread needs to have a priority set on it in order for it to run.
<code class="language-plaintext highlighter-rouge">seL4_TCB_SetPriority(tcb_object.cptr, seL4_CapInitThreadTCB, seL4_MaxPrio);</code>
will give your new thread the same priority as the current thread, allowing it
to be run the next time the seL4 scheduler is invoked.  The seL4 scheduler is invoked
everytime there is a kernel timer tick.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml">https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>

<h3 id="name-the-new-tcb">Name the new TCB</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 10: give the new thread a name */</span>
    <span class="cm">/* hint: we've done thread naming before */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">NAME_THREAD</span><span class="p">(</span><span class="n">tcb_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="s">"libraries-1: thread_2"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>This is a convenience function – sets a name string for the TCB object.</p>

<p>On successful completion this task, the output should not change.</p>

<h3 id="set-the-instruction-pointer">Set the instruction pointer</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/*
     * set start up registers for the new thread:
     */</span>
    <span class="n">UNUSED</span> <span class="n">seL4_UserContext</span> <span class="n">regs</span> <span class="o">=</span> <span class="p">{</span><span class="mi">0</span><span class="p">};</span>

    <span class="cm">/* TASK 11: set instruction pointer where the thread shoud start running */</span>
    <span class="cm">/* hint 1: sel4utils_set_instruction_pointer()
     * void sel4utils_set_instruction_pointer(seL4_UserContext *regs, seL4_Word value);
     * @param regs Data structure in which to set the instruction pointer value
     * @param value New instruction pointer value
     *
     * hint 2: we want the new thread to run the function "thread_2"
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">sel4utils_set_instruction_pointer</span><span class="p">(</span><span class="o">&amp;</span><span class="n">regs</span><span class="p">,</span> <span class="p">(</span><span class="n">seL4_Word</span><span class="p">)</span><span class="n">thread_2</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>Pay attention to the line that precedes this particular task – the line
that zeroes out a new “seL4_UserContext” object. As we previously
explained, seL4 requires you to fill out the Thread Control Block
manually. That includes the new thread’s initial register contents. You
can set the value of the stack pointer, the instruction pointer, and if
you want to get a little creative, you can pass some initial data to
your new thread through its registers.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4utils/sel4_arch_include/x86_64/sel4utils/sel4_arch/util.h">https://github.com/seL4/seL4_libs/blob/master/libsel4utils/sel4_arch_include/x86_64/sel4utils/sel4_arch/util.h</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>
<h3 id="set-the-stack-pointer">Set the stack pointer</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 12: set stack pointer for the new thread */</span>
    <span class="cm">/* hint 1: sel4utils_set_stack_pointer()
     * void sel4utils_set_stack_pointer(seL4_UserContext *regs, seL4_Word value);
     * @param regs  Data structure in which to set the stack pointer value
     * @param value New stack pointer value
     *
     * hint 2: remember the stack grows down!
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">sel4utils_set_stack_pointer</span><span class="p">(</span><span class="o">&amp;</span><span class="n">regs</span><span class="p">,</span> <span class="n">thread_2_stack_top</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>This TASK is just some pointer arithmetic. The cautionary note that the
stack grows down is meant to make you think about the arithmetic.
Processor stacks push new values toward decreasing addresses, so give it
some thought.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4_libs/blob/master/libsel4utils/sel4_arch_include/x86_64/sel4utils/sel4_arch/util.h">https://github.com/seL4/seL4_libs/blob/master/libsel4utils/sel4_arch_include/x86_64/sel4utils/sel4_arch/util.h</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>

<h3 id="write-the-registers">Write the registers</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 13: actually write the TCB registers.  We write 2 registers:
     * instruction pointer is first, stack pointer is second. */</span>
    <span class="cm">/* hint: seL4_TCB_WriteRegisters()
     * int seL4_TCB_WriteRegisters(seL4_TCB service, seL4_Bool resume_target, seL4_Uint8 arch_flags, seL4_Word count, seL4_UserContext *regs)
     * @param service Capability to the TCB which is being operated on.
     * @param resume_target The invocation should also resume the destination thread.
     * @param arch_flags Architecture dependent flags. These have no meaning on either IA-32 or ARM.
     * @param count The number of registers to be set.
     * @param regs Data structure containing the new register values.
     * @return 0 on success
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_WriteRegisters</span><span class="p">(</span><span class="n">tcb_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">0</span><span class="p">,</span> <span class="mi">2</span><span class="p">,</span> <span class="o">&amp;</span><span class="n">regs</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>As explained above, we’ve been filling out our new thread’s TCB for the
last few operations, so now we’re writing the values we’ve chosen, to
the TCB object in the kernel.</p>
<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml">https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>

<h3 id="start-the-new-thread">Start the new thread</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 14: start the new thread running */</span>
    <span class="cm">/* hint: seL4_TCB_Resume()
     * int seL4_TCB_Resume(seL4_TCB service)
     * @param service Capability to the TCB which is being operated on.
     * @return 0 on success
     */</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">error</span> <span class="o">=</span> <span class="n">seL4_TCB_Resume</span><span class="p">(</span><span class="n">tcb_object</span><span class="p">.</span><span class="n">cptr</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>Finally, we tell the kernel that our new thread is runnable. From here,
the kernel itself will choose when to run the thread based on the
priority we gave it, and according to the kernel’s configured scheduling
policy.</p>

<ul>
  <li><a href="https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml">https://github.com/seL4/seL4/blob/master/libsel4/include/interfaces/sel4.xml</a></li>
</ul>

<p>On successful completion this task, the output should not change.</p>
<h3 id="print-something">Print something</h3>
<div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>
    <span class="cm">/* TASK 15: print something */</span>
    <span class="cm">/* hint: printf() */</span>
<span class="err">}</span>
</code></pre></div></div>

<details>
  <summary><em>Quick solution</em></summary>

  <div class="language-c highlighter-rouge"><div class="highlight"><pre class="highlight"><code>    <span class="n">printf</span><span class="p">(</span><span class="s">"thread_2: hallo wereld</span><span class="se">\n</span><span class="s">"</span><span class="p">);</span>
</code></pre></div>  </div>
</details>

<p>For the sake of confirmation that our new thread was executed by the
kernel successfully, we cause it to print something to the screen.</p>

<p>On success, you should see output from your new thread.</p>

<h2 id="links-to-source">Links to source</h2>

<ul>
  <li><code class="language-plaintext highlighter-rouge">sel4_BootInfo</code>:
    <a href="https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo_types.h">https://github.com/seL4/seL4/blob/master/libsel4/include/sel4/bootinfo_types.h</a></li>
  <li><code class="language-plaintext highlighter-rouge">simple_t</code>:
    <a href="https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h">https://github.com/seL4/seL4_libs/blob/master/libsel4simple/include/simple/simple.h</a></li>
  <li><code class="language-plaintext highlighter-rouge">vka_t</code>:
    <a href="https://github.com/seL4/seL4_libs/blob/master//libsel4vka/include/vka/vka.h">https://github.com/seL4/seL4_libs/blob/master//libsel4vka/include/vka/vka.h</a></li>
  <li><code class="language-plaintext highlighter-rouge">allocman_t</code>:
    <a href="https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/allocman.h">https://github.com/seL4/seL4_libs/blob/master/libsel4allocman/include/allocman/allocman.h</a></li>
  <li><code class="language-plaintext highlighter-rouge">name_thread()</code>:
    <a href="https://github.com/seL4/sel4-tutorials/blob/master/libsel4tutorials/src/constructors.c">https://github.com/seL4/sel4-tutorials/blob/master/libsel4tutorials/src/constructors.c</a></li>
</ul>

<p>That’s it for this tutorial.</p>



<p style="text-align: right;">

      Next: <a href="/Tutorials/libraries-2">IPC</a>
</p>

<hr>
    <p><em>Tutorial included from <a href="https://github.com/sel4/sel4-tutorials/blob/master/tutorials/libraries-1/libraries-1.md">github repo</a> <a href="https://github.com/sel4/sel4-tutorials/edit/master/tutorials/libraries-1/libraries-1.md">edit</a></em></p>
  </div>

  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#prerequisites">Prerequisites</a></li>
<li class="toc-entry toc-h2"><a href="#initialising">Initialising</a></li>
<li class="toc-entry toc-h2"><a href="#exercises">Exercises</a>
<ul>
<li class="toc-entry toc-h3"><a href="#obtain-bootinfo">Obtain BootInfo</a></li>
<li class="toc-entry toc-h3"><a href="#initialise-simple">Initialise simple</a></li>
<li class="toc-entry toc-h3"><a href="#use-simple-to-print-bootinfo">Use simple to print BootInfo</a></li>
<li class="toc-entry toc-h3"><a href="#initialise-an-allocator">Initialise an allocator</a></li>
<li class="toc-entry toc-h3"><a href="#obtain-a-generic-allocation-interface-vka">Obtain a generic allocation interface (vka)</a></li>
<li class="toc-entry toc-h3"><a href="#find-the-cspace-root-cap">Find the CSpace root cap</a></li>
<li class="toc-entry toc-h3"><a href="#find-the-vspace-root-cap">Find the VSpace root cap</a></li>
<li class="toc-entry toc-h3"><a href="#allocate-a-tcb-object">Allocate a TCB Object</a></li>
<li class="toc-entry toc-h3"><a href="#configure-the-new-tcb">Configure the new TCB</a></li>
<li class="toc-entry toc-h3"><a href="#name-the-new-tcb">Name the new TCB</a></li>
<li class="toc-entry toc-h3"><a href="#set-the-instruction-pointer">Set the instruction pointer</a></li>
<li class="toc-entry toc-h3"><a href="#set-the-stack-pointer">Set the stack pointer</a></li>
<li class="toc-entry toc-h3"><a href="#write-the-registers">Write the registers</a></li>
<li class="toc-entry toc-h3"><a href="#start-the-new-thread">Start the new thread</a></li>
<li class="toc-entry toc-h3"><a href="#print-something">Print something</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#links-to-source">Links to source</a></li>
</ul>
</div>

  
</div>
<script src="/assets/js/toggle-markdown.js"></script>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Mon Jan 6 18:52:01 2025 +1100 df31e5ccb8
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/Tutorials/libraries-1.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/Tutorials/libraries-1.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
